PR #18 landed the remaining three ownerListInvariant proofs and
replaced the unprovable stronglyAcyclic (antisymmetry of reachable,
false on Safe's circular list) with uniquePredecessor. Update the
article to match:

- Proof status: 9/12 -> 12/12, Proofs.lean sorry-free; all table
  cells flipped to "proven"
- "What these invariants cover": four properties -> three (drop
  the stronglyAcyclic bullet)
- "How this was proven": rewrite the strong-acyclicity paragraph
  around unique-predecessor, with the SENTINEL -> o -> SENTINEL
  counter-example
- Hypotheses: collapse eight entries into four. Solidity require
  guards merged; hPreInv absorbs hClean; hOwnerInList and
  hOldNePrev combined; hStrongAcyclic removed; uniquePredecessor
  added as the new load-bearing structural fact
- Drop the "view open theorems" link (OpenProofs.lean is now an
  index)

* Add Safe owner list reachability invariant research page

New case study page for the formally verified inListReachable invariant
of the Safe OwnerManager linked list, proven using Verity and Lean 4.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

* Fix research ordering and shared hypothesis UI

* Add Bun-based CI workflow

* Pin GitHub Actions to Node 24 runtime

* Update GitHub Actions to current major versions

* Optimize CI workflow execution

* Update Safe research page for expanded OwnerManager benchmark

Reflects verity-benchmark PR #18 which extends the Safe case from
addOwner-only to all four ownership-mutating functions (setupOwners,
addOwner, removeOwner, swapOwner) and three invariant families
(inListReachable, ownerListInvariant, acyclicity).

Key changes:
- Title broadened to "Safe Owner List Invariants"
- SafeGuarantee now shows the ownerListInvariant biconditional
- "What these invariants cover" lists all three invariant families
- "How this was proven" describes all four function models
- Added proof status table (1 proven, 11 open benchmark tasks)
- Hypotheses updated: added hPrevLink (GS205), hClean (setupOwners),
  reclassified hAcyclic and hFreshInList as provable properties
- Links updated for new Specs.lean line numbers and OpenProofs.lean

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

* Show all three invariants in hero guarantee toggle

Display inListReachable, ownerListInvariant, and acyclic as a
stacked list with English/formal toggle. Each invariant label
links to its definition in Specs.lean.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

* Update Safe research page to reflect full benchmark state

- Extract shared Hypothesis component from duplicated code in both
  research pages (bugbot fix)
- Move safe-owner-reachability to top of research list as newest entry
  (bugbot fix)
- Update page content: all 4 functions modeled (setupOwners, addOwner,
  removeOwner, swapOwner), 6/6 benchmark proofs complete
- Update SafeGuarantee to show ownerListInvariant (biconditional)
  instead of just inListReachable
- Add proof status table, stronglyAcyclic hypothesis, and updated
  hypothesis descriptions (hOwnerInList, hOldNePrev, hStrongAcyclic)
- Update page title and metadata to "Safe Owner List Invariants"

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

* Remove unused ExternalLinkIcon import from SafeGuarantee

The INVARIANTS-based multi-row layout uses plain <a> tags for
invariant labels, so ExternalLinkIcon is no longer referenced.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

* Add stronglyAcyclic invariant to hero and disclosure

Reflects the new stronglyAcyclic definition (antisymmetry of
reachability) added in verity-benchmark PR #18, which captures
Certora's reach_invariant axiom and is required by removeOwner
and swapOwner proofs.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

* Fix proof status table: 9 of 12 theorems proven

The table was showing only 6 benchmark tasks and incorrectly
listing removeOwner/swapOwner acyclicity and setupOwners
ownerListInvariant as open. Cross-referencing Proofs.lean (0 sorry)
shows 9 theorems are proven. Only 3 ownerListInvariant preservation
theorems (addOwner, removeOwner, swapOwner) remain open.

Switched to a compact function x invariant grid matching the
actual proof state.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

* Polish Safe owner reachability research page and hero

- SafeGuarantee: English summary wording, formal-only math (no Lean names),
  centered sizing tuned vs Lido hero
- Page: disclosure lists four invariants; prose and links (OwnerManager.sol,
  Verity Contract.lean); remove em dashes; How this was proven intro ties
  Verity model to Solidity source

Made-with: Cursor

* Safe reachability page: TikZ diagram, circular list wording, copy tweaks

- Add TikZDiagram (TikZJax) for owners linked-list figure
- Disclosure: describe invariant as proper loop-free circular linked list
- SafeGuarantee and intro copy adjustments

Made-with: Cursor

* Safe reachability page: 12/12 proven, drop stronglyAcyclic story

PR #18 landed the remaining three ownerListInvariant proofs and
replaced the unprovable stronglyAcyclic (antisymmetry of reachable,
false on Safe's circular list) with uniquePredecessor. Update the
article to match:

- Proof status: 9/12 -> 12/12, Proofs.lean sorry-free; all table
  cells flipped to "proven"
- "What these invariants cover": four properties -> three (drop
  the stronglyAcyclic bullet)
- "How this was proven": rewrite the strong-acyclicity paragraph
  around unique-predecessor, with the SENTINEL -> o -> SENTINEL
  counter-example
- Hypotheses: collapse eight entries into four. Solidity require
  guards merged; hPreInv absorbs hClean; hOwnerInList and
  hOldNePrev combined; hStrongAcyclic removed; uniquePredecessor
  added as the new load-bearing structural fact
- Drop the "view open theorems" link (OpenProofs.lean is now an
  index)

---------

Co-authored-by: Claude <noreply@anthropic.com>